'''
Created on 06-09-2011

@author: kc262414
'''
import unittest
from dataStructs.formulaSet import Theory
from dataStructs.definitions import Formula, OrFormula
from parsing.parser import sents_parse_string
from config.config import getValidParseExamplesDirs


class testInstantizartion(unittest.TestCase):
    th=0;

    def loadTheory(self, dataBaseFile):
        kb =  getValidParseExamplesDirs() +dataBaseFile 
        th = Theory(kb)    
        return th

    def setUp(self):
        self.th = Theory()
        self.th.addFormula('a')
        self.th.addFormula('b')


    def tearDown(self):
        pass


    def testOnSigleVar(self):
        self.th.addFormula('A||A')
        self.th.instantine()
        lstTh = self.th.theory
        self.assertEqual(2+2,len(lstTh))
        formAA = sents_parse_string("a||a")[0]
        formBB = sents_parse_string("b||b")[0]
        self.assertTrue(formAA in lstTh)
        self.assertTrue(formBB in lstTh)
        
    def testOnMulitpleVar(self):
        self.th.addFormula('A || B && C')
        self.th.instantine()
        lstTh = self.th.theory
        self.assertEqual(8+2, len(lstTh))
        formAAB = sents_parse_string("a || a && b")[0]
        self.assertTrue(formAAB in lstTh)
        
    def testRel(self):
        self.th.addFormula('r(A,A,B)')
        self.th.instantine()
        lstTh = self.th.theory
        self.assertEqual(4+2, len(lstTh))
        formAAB = sents_parse_string("r(a,a,b)")[0]
        self.assertTrue(formAAB in lstTh)
        
      
    def test3TimesWithUniversal(self):
        th = self.loadTheory("/then3timesWithUniversal.wn")
        th.instantine()
        self.assertTrue( 
                    str(th.theory) == 
                    '[ ( b -> c ) ,  ( b -> b ) ,  ( b -> d ) ,  ( c -> b ) ,  ( d -> c ) , d]')
        
        
if __name__ == "__main__":
    #import sys;sys.argv = ['', 'Test.testName']
    unittest.main()
    